\documentclass[a4paper]{article}

\usepackage[spanish]{babel}
\usepackage[latin1]{inputenc}
\usepackage{bbm}
\usepackage{framed}
\input{macrosAlgo1}

\textheight=23.94cm
\textwidth=17cm
\topmargin=-1cm
\oddsidemargin=-1.5cm
\renewcommand{\baselinestretch}{1.5}
\parindent=1.5cm 
\newcommand{\comen}[2]{%

\begin{framed}	
\noindent \textsf{#1:} #2
\end{framed}
}



\begin{document}

\materia{Algoritmos y Estructura de Datos I}
\cuatrimestre{1}
\anio{2012}

\fecha{30 de Marzo de 2012}

\nombre{\LARGE TPE OJOTA (Organizaci\'on de Juegos Ol\'impicos Tp de Algoritmos 1) v1.0}

\titulotp


\section{Tipos}

\input{tipos/tipos.tex}

\section{Atleta}
\input{tipos/atleta.tex}

\begin{problema}{entrenarNuevoDeporte}{a: Atleta, d: Deporte, c: \ent}{}
\requiere[capacidadEnRango]{0 \leq c \leq 100}
\modifica{a}
\asegura[nombre]{nombre(a)==nombre(pre(a))}
\asegura[sexo]{sexo(a)==sexo(pre(a))}
\asegura[aNoNacimiento]{{aNoNacimiento}(a)=={aNoNacimiento}(pre(a))}
\asegura[nacionalidad]{nacionalidad(a)==nacionalidad(pre(a))}
\asegura[ciaNumber]{ciaNumber(a)==ciaNumber(pre(a))}
\asegura[noRepetirDeportes]{if$ $d \in deportes(pre(a))$ $then deportes(pre(a))==deportes(a)$ $else$ $mismos(deportes(a), cons(d, deportes(pre(a)))}
\asegura[capacidad]{capacidad(a, d)==if$ $d \in deportes(pre(a))$ $then capacidad(pre(a), d)$ $else c}
\end{problema}



\section{Competencia}

\input{tipos/competencia.tex}

\begin{problema}{finalizarCompetencia}{c:competencia,posiciones:[Atleta],control:[(atleta,Bool)]}{}{}
\requiere{mismos(posiciones,participantes(c))}
\requiere{incluida([x|x \leftarrow prm (control)],participantes(c))}
\modifica{c}
\asegura{categoria(c)==categoria(pre(c))}
\asegura{mismos(participantes(c), participantes(pre(c)))}
\asegura{finalizada(c)==True}
\asegura{ranking(c)==posiciones}
\asegura{mismos(lesTocoControl(c),control)}
\asegura{leDioPositivo(c,a)$ $If$ $a \in [x|x \leftarrow control, x \leftarrow sgdo(control)==True]$ $then$ $True$ $else$ $False}
\end{problema}


\begin{problema}{linfordChristie}{c: Competencia, a: Atleta}{[Competencia]}{}
\requiere[]{finalizada(c)==false}
\requiere[]{a\in participantes(c)}
\modifica{participantes(c)}
\asegura[]{mismos (pre(participantes(c),a:participantes(pre(c)))}
\asegura[]{categoria(c)==categoria(pre(c))}
\asegura[]{finalizada(c)==finalizada(pre(c))}
\end{problema}

\begin{problema}{gananLosMasCapaces}{c: Competencia}{Bool}{}
\requiere[]{finalizada(c)==true}
\asegura[]{ranking(c)==ordenarPorCapacidad(a, d)}
\end{problema}

\begin{problema}{sancionarTramposos}{c: Competencia}{}
\requiere[competenciaFinalizada]{finalizada(c)==true}
\modifica{c}
\asegura[mismaCategoria]{categoria(c)==categoria(pre(c))}
\asegura[mismosParticipantes]{mismos(participantes(c),participantes(pre(c)))}
\asegura[yaFinalizada]{finalizada(c)==finalizada(pre(c))}
\asegura[controlados]{lesTocoControlAntiDoping(c)==lesTocoControlAntiDoping(pre(c))}
\asegura[lesDioPositivo]{lesDioPositivo(c, a)==lesDioPositivo(pre(c), a)}
\asegura[eliminarDelRanking]{mismos(concat([x\leftarrow lesTocoControlAntiDoping(c), leDioPositivo(c, x)], ranking(c)), \newline ranking(pre(c)))}
\asegura[reordenada]{ordenadaDeAcuerdoA(ranking(c), ranking(pre(c)))}
\end{problema}

\section{JJOO}
\input{tipos/jjoo.tex}

\begin{problema}{dePaseo}{j:JJOO}{[Atleta]}{}
 \asegura {mismos( result , (\forall a \leftarrow atletas (j), a \notin [x|x \leftarrow participantes(c), c\leftarrow competencias(j)]))}
\end{problema}

\begin{problema}{medallero}{j: JJOO}{[(Pais,[\ent])]}
\asegura{sinRepetidos(result)}
\asegura{estaOrdenadaSegunMedallero(result)}
\asegura{(\forall p2 \selec [prm(p1)|p1 \selec result]) p2 \in concat(paisesOro(j),paisesPlata(j),paisesBronce(j))}
\asegura{(\forall p2 \selec concat(paisesOro(j),paisesPlata(j),paisesBronce(j)) p2 \in result}
\asegura{(\forall c \selec [(prm(p1),sgd(p1)) | p1 \selec result]) sgd(c)==cantMedallasPorPais(prm(c))}
\end{problema}


\begin{problema}{boicotPorDisciplina}{$j: JJOO, cat: (Deporte, Sexo), p: Pais)$}{$\ent$}{}
\requiere[boicotPosible]{finalizada([c|c\leftarrow competencias(j), categoria(c)==cat]_{0}==False}
\modifica{j}
\asegura[noCambiaANo]{aNo(j)==aNo(pre(j))}
\asegura[noCambiaAtletas]{mismos(atletas(j), atletas(pre(j))}
\asegura[noCambiaCantidadDias]{cantDias(j)==cantDias(pre(j))}
\asegura[noCambiaCronograma]{cronograma(j)==cronograma(pre(j))}
\asegura[noCambiaJornadaActual]{jornadaActual(j)==jornadaActual(pre(j))}
\asegura[eliminarDeCompetencia]{(\forall a_{1} \in participantes(c), c\leftarrow competencias(j), categoria(c)==cat) nacionalidad(a_{1})\neq p}
\asegura[agregarLosQueVan]{(\forall a_{1} \in participantes(c), c\leftarrow competencias(j), categoria(c)==cat, nacionalidad(a_{1})\neq p) a_{1} \in (participantes(c), c\leftarrow competencias(pre(j)), categoria(c)==cat)}
\asegura[queNoMeSobren]{(\forall a_{1} \in participantes(c), c\leftarrow competencias(j), categoria(c)==V) a_{1} \in (participantes(c), c\leftarrow competencias(pre(j), categoria(c)==v)}
\asegura[result]{result==|[x|x \leftarrow participantes(competencias(pre(j)), categoria(c)==cat]|}
\end{problema}

\begin{problema}{losMasFracasados}{j:JJOO,p:pais}{[Atleta]}{}
\asegura{mismos (result,[a|a \in losQueMasParticiparon(p,j)\wedge(|medallasDelAtleta(a,j)|==0)])}
\end{problema}



\begin{problema}{liuSong}{j:JJOO, a:Atleta, p:Pais}{[Atleta]}{}
\requiere{\neg ( \exists x \leftarrow atletas (j)), igualSalvoPais (a,x,p)}
\modifica {j}
\asegura {aNo(j)==aNo(pre(j))}
\asegura {cantDias(j)==cantDias(pre(j))}
\asegura {cronograma(j,d)==cronograma(pre(j,d))}
\asegura {jornadaActual(j)==jornadaActual(pre(j))}
\asegura {|atletas(j)|==|atletas(pre(j))|}
\asegura {(\forall x1 \leftarrow atletas (pre(j)), x==a) (\exists x2 \leftarrow atletas(j),igualSalvoPais(x1,x2,p)}
\end{problema}

\begin{problema}{stevenBradbury}{j: JJOO}{Atleta}
\requiere{|ganaronOro(j)| > 0}  %ac� queria poner ganaronOro(j) distinto de lista vacia pero no me sali� :P supongo q esto es lo mismo%
\asegura{result \in ganaronOro(j)}
\asegura{(\forall c \selec capacidadesDeportesGanoOro(a,j),a \selec ganaronOro(j), a \neq result)\newline(\exists m \selec capacidadesDeportesGanoOro(result,j) m \leq c}
\end{problema}

\begin{problema}{uyOrdenadoAsiHayUnPatron}{j: JJOO}{Bool}{}
\asegura[]{result==hayPatron(listaDeMejores(j))}
\end{problema}

\begin{problema}{sequiaOlimpica}{(j:JJOO)}{[Pais]}{}
\requiere {incluida(result,paisesQueParticiparon(j,dia))==true}
\asegura{(p\in result)\leftrightarrow (sequiaDelPais(j,dia,p)\geq sequiaDelPais(j,dia,q) \forall q\in paisesQueParticiparon(j,dia),[1\leq dia<jornadaActual(j))}
\end{problema}

\begin{problema}{transcurrirDia}{j: JJOO}{}
\modifica{j}
\asegura{aNo(j)==aNo(pre(j))}
\asegura{cantdias(j)==cantDias(pre(j))}
\asegura{jornadaActual(j)==jornadaActual(pre(j))+1}
\asegura{(\forall c \selec cronograma(j,jornadaActual(j)) finalizada(c) \wedge ordenadaPorCapacidad(ranking(c), sgd(categoria(c))) \newline \wedge antiDopingAUnUnico(c)}
\asegura{leDioPositivo5PorCiento(cronograma(j ,jornadaActual(j)))} 
\end{problema}

\newpage

\section{Auxiliares}
\input{auxiliaresTipos.tex}
\aux{antiDopingAUnUnico}{c: Competencia}{Bool}{|lesTocoControlAntiDoping(c)|==1}
\aux{atletasDelPais}{(p:Pais,j:JJOO)}{[Atleta]}{[a|(nacionalidad(a)==p)\wedge(a\in atletas(j))]}
\aux{atletasOroDiario}{j: JJOO, dia: \ent}{[Atleta]}{[cab(ranking(c))|c \selec cronograma(j,dia)]}
\aux{cantMedallasDeOroPorDia}{p: Pais, dia: \ent, j: JJOO}{\ent}{cuenta(p,paisesOroDiario(j,dia))}
\aux{cantMedallasPorPais}{p: Pais, j: JJOO}{[\ent]}{\newline[cuenta(p,paisesOro(j)),cuenta(p,paisesPlata(j)),cuenta(p,paisesBronce(j))]}
\aux{capacidadesDeportesGanoOro}{a: Atleta, j: JJOO}{[\ent]}{[capacidad(a,d) | d \selec prm(categoria(c)), c \selec competencias(j), d \in deportes(a), cab(ranking(c) == a]}
\aux{compParticipadas}{a:Atleta,j:JJOO}{[Competencia]}{[c|(c\in cronograma(j))\wedge(a\in top3Medallas(c,j))]}
\aux{escaleraMasLarga}{(j:JJOO,dia: \ent,p:Pais)}{[\ent]}{cab([l_1|\forall l_1,l_2, incluida(l_1,todasLasEscaleras\\(obtenerIndices(medallasEnLosJuegos(j,dia,p),0)))==true, incluida(l_2,todasLasEscaleras\\(obtenerIndices(medallasEnLosJuegos(j,dia,p),0)))==true, |l_1|\geq|l_2|]}
\aux{enEsteDiaGanoOro}{(j:JJOO,dia:\ent,p:Pais)}{\ent}{\beta((\forall c \selec cronograma(j,dia))(\exists a \selec ranking(c), a==cab(ranking(c))) nacionalidad(a)==p)}
\aux{esGrandeYEstaOrdenadoLexicograficamente}{$x: (string, \ent), L: [(string, \ent)]$}{Bool}{(\forall y \in L) sgd(x) \geq sgd(y), prm(x)<prm(y) }
\aux{esMasGrandeQueTodos}{x: T, L: [T]}{Bool}{(\forall y \in L) x > y}
\aux{ganaronBronce}{j: JJOO}{[Atleta]}{[indice(x,2)|x\selec (rankingCompetencias(j))]}
\aux{ganaronOro}{j: JJOO}{[Atleta]}{[cab(x)|x\selec (rankingCompetencias(j))]}
\aux{ganaronPlata}{j: JJOO}{[Atleta]}{[indice(x,1)|x\selec (rankingCompetencias(j))]}
\aux{hayPatron}{L: [T]}{Bool}{indice(L, [0..|l|)==X_{cabeza(cola(encontrarIndices(X_{0}, L))+[0..|l|)}}
\aux{igualSalvoPais}{x1,x2:atleta, p:pais}{Bool}{\newline nombre(x1)==nombre(x2)\wedge sexo(x1)==sexo(x2) \wedge aNoNacimiento(x1)==aNoNacimiento(x2)\wedge \newline nacionalidad(x2)==p\wedge ciaNumber(x1)==ciaNumber(x2)\wedge deportes(x1)==deportes(x2) \wedge  (\forall d1 \leftarrow deportes(x1), d2 \leftarrow deportes (x2))(capacidad(x1,d1)==capacidad(x2,d2))}
\aux{leDioPositivo5PorCiento}{c: [Competencia]}{Bool}{|[a | a \selec lesTocoControlAntiDoping(c1), c1 \selec c, leDioPositivo(c1,a)]| \leq |[[a | a \selec lesTocoControlAntiDoping(c1), c1 \selec c]| * 0.05}
\aux{listaDeMejores}{j: JJOO}{[Pais]}{[x|x\leftarrow mejorPorDia(z: \ent, j: JJOO), z\leftarrow [1..jornadaActual(j))]}
\aux {losQueMasParticiparon}{(p:Pais, j:JJOO)}{[Atleta]}{
[a|a \in atletasDelPais(p)\wedge(\forall b \in atletasDelPais(p),\\|compParticipadas(a)| \geq |compParticipadas(b)|)]}
\aux{maximo2}{$L: [(Pais,\ent)]$}{Pais}{[x|x\leftarrow prim(l_{i}), l_{i} \leftarrow L, esMasGrandeQueTodos(x, L)\newline$ $\vee$  $esGrandeYEstaOrdenadoLexicograficamente(x, L)]}
\aux{medallasEnLosJuegos}{(j:JJOO,dia:\ent,p:Pais)}{\ent}{[z|z==enEsteDiaGanoOro(j,dia,p),\\dia\leftarrow [1..jornadaActual(j))]}
\aux{medallasPorDiaPorPais}{n: \ent, j: JJOO}{[(p, \ent)]}{[(p, cantMedallasDeOroPorDia(p, d, j)), p\leftarrow nacionalidad(a), a \leftarrow atletas(j), d == z]}
\aux{mejorPorDia}{z: \ent, j: JJOO}{Pais}{[x|x\leftarrow maximo2(medallasPorDiaPorPais(z, j)]_{0}}
\aux{obtenerIndice}{L:[T], a: T}{\ent}{[i|i\leftarrow [0..|l|), li==a]_{0}}
\aux{obtenerIndices}{$L:[T], a: T$}{$[\ent]$}{[i|i\leftarrow [0..|l|), li==a]}
\aux{ordenarPorCapacidad}{a:[Atletas], d:Deporte}{Bool}{(\forall x_{i, j} \in L), capacidad(x_{1}, d) > capacidad(x_{j}, d), i<j}
\aux{ordenRelativo}{$L_{1}, L_{2}: [T]$}{Bool}{\forall X_{i}, X_{j} \in L_{1}$ $if$ $obtenerIndice(L_{2}, X_{i}) < obtenerIndice(L_{2}, X_{j})$ $then$ $i < j$ $else$ $i \geq j}
\aux{estaOrdenadaSegunMedallero}{[(Pais, [\ent])}{\forall l_{i}, l_{j}, si cab(seg(l_{i}))>cab(seg(l_{j} \rightarrow i<j, si cab(seg(l_{i}))==cab(seg(l_{j})) \wedge indice(seg(l_{i}, 1))>indice(seg(l_{j}, 1)) \rightarrow i<j, si cab(seg(l_{i}))==cab(seg(l_{j})) \wedge indice(seg(l_{i}, 1))==indice(seg(l_{j}, 2)) \wedge indice(seg(l_{i}, 2))>indice(seg(l_{j}, 2)) \rightarrow i<j}
\aux{paisesOroDiario}{j: JJOO, dia: \ent}{[Pais]}{[nacionalidad(a)|a \selec atletasOroDiario(j,dia)]}
\aux{paisesOro}{j: JJOO}{[Pais]}{[nacionalidad(x)|x \selec ganaronOro(j)]}
\aux{paisesPlata}{j: JJOO}{[Pais]}{[nacionalidad(x)|x \selec ganaronPlata(j)]}
\aux{paisesBronce}{j: JJOO}{[Pais]}{[nacionalidad(x)|x \selec ganaronBronce(j)]}
\aux{paisesQueParticiparon}{(j:JJOO,dia:\ent}{Pais}{[p|a\in participantes(c),c\in cronograma(j,dia),\\p==nacionalidad(a)]}
\aux{rankingCompetencias}{j: JJOO}{[[Atleta]]}{[ranking(c)|d \selec [1..cantDias(j)], c \selec cronograma(j, d)]}
\aux{sequiaDelPais}{(j:JJOO,dia: \ent,p:Pais)}{\ent }{|escaleraMasLarga(j,dia,p)|}
\aux{todasLasEscaleras}{(l:[T])}{[[\ent]]}{[(a,b)|a,b\in l,incluido([a..b],l)==true]}
\aux{top3Medallas}{(c:Competencia,j:JJOO)}{[Atleta]}{[a|(a\in atletas(j))\wedge(a\in sub(ranking(c),0,2))\wedge(c\in cronograma(j)]}

\end{document}
